FDL - Step of Proof: complete_nat_ind_with

Step of Proof: complete_nat_ind_with_y

9,38

Inference at * 1
Iof proof for Lemma complete nat ind with y:

(

P,g. Y(

f,x. g(x,f)))

(

P:(

{k}). (

. (

i. P(j))

P(i))

(

. P(i)))

by ((MemberEqCD)

CollapseTHEN (IfLab `subterm`

C((MemberEqCD)

CollapseTHEN (

CIfLab `subterm` Id (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t

C) inil_term)))

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t

C) inil_term)))

C1: .....subterm..... T:t1:n

C1: 1. P :

{k}

C1: 2. g :

. (

i. P(j))

P(i)

C1:

f,x. g(x,f))

(

. P(i))

Definitions x(s), P Q, , , x:A. B(x), t T, P Q, i j < k, {i..j}

Lemmas le wf, int seg wf, nat wf

Definitions	x(s), P Q, , , x:A. B(x), t T, P Q, i j < k, {i..j}
Lemmas	le wf, int seg wf, nat wf